Require Import ZArith.
Open Scope Z_scope.

Inductive reg : Set :=	(* registers *)
  | r0 : reg
  | r1 : reg
  | r2 : reg
  | r3 : reg
  | r4 : reg
  | r5 : reg
  | r6 : reg
  | r7 : reg.


Definition beq_reg (r1 r2 : 	(* comp r1 r2, ret bool *)
                    reg) :=
  match r1, r2 with
  | r0, r0 => true
  | r1, r1 => true
  | r2, r2 => true
  | r3, r3 => true
  | r4, r4 => true
  | r5, r5 => true
  | r6, r6 => true
  | r7, r7 => true
  | _, _ => false
  end.

Inductive rfile : Set :=	(* register file *)
  | emptyR : rfile
  | consR : rfile -> reg -> Z -> rfile.

Fixpoint lookupR (rf : rfile) (r : reg) {struct rf} : Z :=
  	(* look up reg file *)
 match rf with
 | emptyR => 0
 | consR rf' r' i => if beq_reg r r' then i else lookupR rf' r
 end.

Definition updateR (rf : rfile) (r : reg) (i : Z) : rfile :=
   (* update reg file *)
  consR rf r i.

Definition heap:Set := Z->Z.
Definition hr(h:heap)(a:Z):Z := h a.
Definition hw(h:heap)(a:Z)(v:Z):Z->Z := fun (a1:Z) =>
  if (Zeq_bool a a1) then v else (h a1).

Lemma w1: forall h a v, hr (hw h a v) a = v.
Proof.
  intros.
  unfold hr; unfold hw.
  unfold Zeq_bool. 
  rewrite (Zcompare_refl a).
  reflexivity.
Qed.

Lemma w2: forall h a a1 v, a<>a1 ->  hr (hw h a v) a1 = h a1. 
Proof.
  intros.
  unfold hr; unfold hw.
  unfold Zeq_bool.
  assert (Hz := Ztrichotomy_inf a a1).
  destruct Hz as [[z | z] | z];
    try (rewrite z; reflexivity).
  subst a.
  elimtype False.
  apply H; reflexivity.
Qed.

Lemma f_vc: forall i : Z, ((i)>=(0)) -> (((i)+(1))>=(1)).
Proof.
  intros.
  cut (i+1>=0+1).
  intros.
  replace (0+1) with 1 in H0.
  apply H0.
  simpl.
  reflexivity.
  apply Zle_ge.
  apply Zplus_le_compat_r.
  apply Zge_le.
  apply H.
Qed.

Lemma f_vc': forall (hp:heap) (rf:rfile),
  ( (hr hp ((lookupR rf r7) + 8))>=0)->(((hr hp ((lookupR rf r7) + 8))+1)>=1).
Proof.
  intros.
  apply f_vc.
  apply H.
Qed.
Print f_vc'.
Print f_vc.
(*
Lemma not_eq: (-79<>46).
Proof.
  auto with zarith.
Qed.
Print not_eq.
Print not_eq_subproof2.

Lemma Asst_alloc_list: forall (R:rfile) (H:heap),True.
Proof.
  intros.
  trivial.
Qed.
Lemma Asst_L1: forall (R:rfile) (H:heap),True.
Proof.
  intros.
  trivial.
Qed.
Lemma Asst_L0: forall (R:rfile) (H:heap),(lookupR R r0)=(6).
Proof.
*)